Новая философская энциклопедия - вывод логический

В ряде случаев логический вывод определяется так, что на использование некоторых правил накладываются ограничения. Напр., в аксиоматических исчислениях, являющихся вариантами классической логики предикатов первого порядка и содержащих среди правил вывода только модус поненс  и правило обобщения, логический вывод часто определяется так, что на использование правила обобщения накладывается ограничение: любое применение правилам обобщения в таково, что переменная, по которой ироввдитея обобюение в этом применении правила обобщения, не входит ни в одну посылку, предшествующую в нижней формуле этого применения правила обобщения. Цель этого ограничения обеспечить ряд полезных с точки зрения логики свойств вывода (напр., выполнение для простых форм дедукции теоремы). Существуют определения логического вывода (как для аксиоматических, так и для исчислений других типов), которые (1) задают логический вывод не только из множества посылок, но допускают другие формы организации посылок (напр., списки или последовательности), (2) структурируют вывод не только линейно, но, напр., в форме дерева, (3) имеют явно выраженный индуктивный характер; при этом индуктивное определение  вывода может вестись как по одной переменной (напр., по длине вывода), так и по нескольким переменньм (напр., по длине логического вывода и по числу его посылок), (4) содержат формализацию зависимости между формулами в логическом выводе, и многие другие определения логического вывода, обусловленные иными способами формализации и аксиоматизации классических и неклассических систем логики. О некоторых из них см. в ст. Аналитических таблиц метод. Семиотика, Исчисление секвенций.

В. М. Попов